(set-logic QF_LRA)
(set-info :source |
SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
information.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Bool)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Bool)
(declare-fun x_24 () Real)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Bool)
(declare-fun x_27 () Bool)
(declare-fun x_28 () Bool)
(declare-fun x_29 () Bool)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Real)
(declare-fun x_33 () Bool)
(declare-fun x_34 () Bool)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Bool)
(declare-fun x_39 () Bool)
(declare-fun x_40 () Real)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Bool)
(declare-fun x_47 () Real)
(declare-fun x_48 () Bool)
(declare-fun x_49 () Bool)
(declare-fun x_50 () Bool)
(declare-fun x_51 () Bool)
(declare-fun x_52 () Bool)
(declare-fun x_53 () Bool)
(declare-fun x_54 () Real)
(declare-fun x_55 () Bool)
(declare-fun x_56 () Bool)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Bool)
(declare-fun x_64 () Bool)
(declare-fun x_65 () Real)
(declare-fun x_66 () Bool)
(declare-fun x_67 () Bool)
(declare-fun x_68 () Bool)
(declare-fun x_69 () Bool)
(declare-fun x_70 () Bool)
(declare-fun x_71 () Bool)
(declare-fun x_72 () Real)
(declare-fun x_73 () Bool)
(declare-fun x_74 () Bool)
(declare-fun x_75 () Real)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Real)
(declare-fun x_81 () Bool)
(declare-fun x_82 () Bool)
(declare-fun x_83 () Real)
(declare-fun x_84 () Bool)
(declare-fun x_85 () Bool)
(declare-fun x_86 () Bool)
(declare-fun x_87 () Bool)
(declare-fun x_88 () Bool)
(declare-fun x_89 () Bool)
(declare-fun x_90 () Real)
(declare-fun x_91 () Bool)
(declare-fun x_92 () Bool)
(declare-fun x_93 () Real)
(declare-fun x_94 () Real)
(declare-fun x_95 () Real)
(declare-fun x_96 () Real)
(declare-fun x_97 () Real)
(declare-fun x_98 () Real)
(declare-fun x_99 () Bool)
(declare-fun x_100 () Bool)
(declare-fun x_101 () Real)
(declare-fun x_102 () Bool)
(declare-fun x_103 () Bool)
(declare-fun x_104 () Bool)
(declare-fun x_105 () Bool)
(declare-fun x_106 () Bool)
(declare-fun x_107 () Bool)
(declare-fun x_108 () Real)
(declare-fun x_109 () Bool)
(declare-fun x_110 () Bool)
(declare-fun x_111 () Real)
(declare-fun x_112 () Real)
(declare-fun x_113 () Real)
(declare-fun x_114 () Real)
(declare-fun x_115 () Real)
(declare-fun x_116 () Real)
(declare-fun x_117 () Bool)
(declare-fun x_118 () Bool)
(declare-fun x_119 () Real)
(declare-fun x_120 () Bool)
(declare-fun x_121 () Bool)
(declare-fun x_122 () Bool)
(declare-fun x_123 () Bool)
(declare-fun x_124 () Bool)
(declare-fun x_125 () Bool)
(declare-fun x_126 () Real)
(declare-fun x_127 () Bool)
(declare-fun x_128 () Bool)
(declare-fun x_129 () Real)
(declare-fun x_130 () Real)
(declare-fun x_131 () Real)
(declare-fun x_132 () Real)
(declare-fun x_133 () Real)
(declare-fun x_134 () Real)
(declare-fun x_135 () Bool)
(declare-fun x_136 () Bool)
(declare-fun x_137 () Real)
(declare-fun x_138 () Bool)
(declare-fun x_139 () Bool)
(declare-fun x_140 () Bool)
(declare-fun x_141 () Bool)
(declare-fun x_142 () Bool)
(declare-fun x_143 () Bool)
(declare-fun x_144 () Real)
(declare-fun x_145 () Bool)
(declare-fun x_146 () Bool)
(declare-fun x_147 () Real)
(declare-fun x_148 () Real)
(declare-fun x_149 () Real)
(declare-fun x_150 () Real)
(declare-fun x_151 () Real)
(declare-fun x_152 () Real)
(declare-fun x_153 () Bool)
(declare-fun x_154 () Bool)
(declare-fun x_155 () Real)
(declare-fun x_156 () Bool)
(declare-fun x_157 () Bool)
(declare-fun x_158 () Bool)
(declare-fun x_159 () Bool)
(declare-fun x_160 () Bool)
(declare-fun x_161 () Bool)
(declare-fun x_162 () Real)
(declare-fun x_163 () Bool)
(declare-fun x_164 () Bool)
(declare-fun x_165 () Real)
(declare-fun x_166 () Real)
(declare-fun x_167 () Real)
(declare-fun x_168 () Real)
(declare-fun x_169 () Real)
(declare-fun x_170 () Real)
(declare-fun x_171 () Bool)
(declare-fun x_172 () Bool)
(declare-fun x_173 () Real)
(declare-fun x_174 () Bool)
(declare-fun x_175 () Bool)
(declare-fun x_176 () Bool)
(declare-fun x_177 () Bool)
(declare-fun x_178 () Bool)
(declare-fun x_179 () Bool)
(declare-fun x_180 () Real)
(declare-fun x_181 () Bool)
(declare-fun x_182 () Bool)
(declare-fun x_183 () Real)
(declare-fun x_184 () Real)
(declare-fun x_185 () Real)
(declare-fun x_186 () Real)
(declare-fun x_187 () Real)
(declare-fun x_188 () Real)
(declare-fun x_189 () Bool)
(declare-fun x_190 () Bool)
(declare-fun x_191 () Real)
(declare-fun x_192 () Bool)
(declare-fun x_193 () Bool)
(declare-fun x_194 () Bool)
(declare-fun x_195 () Bool)
(declare-fun x_196 () Bool)
(declare-fun x_197 () Bool)
(declare-fun x_198 () Real)
(declare-fun x_199 () Bool)
(declare-fun x_200 () Bool)
(declare-fun x_201 () Real)
(declare-fun x_202 () Real)
(declare-fun x_203 () Real)
(declare-fun x_204 () Real)
(declare-fun x_205 () Real)
(declare-fun x_206 () Real)
(declare-fun x_207 () Bool)
(declare-fun x_208 () Bool)
(declare-fun x_209 () Real)
(declare-fun x_210 () Bool)
(declare-fun x_211 () Bool)
(declare-fun x_212 () Bool)
(declare-fun x_213 () Bool)
(declare-fun x_214 () Bool)
(declare-fun x_215 () Bool)
(declare-fun x_216 () Real)
(declare-fun x_217 () Bool)
(declare-fun x_218 () Bool)
(declare-fun x_219 () Real)
(declare-fun x_220 () Real)
(declare-fun x_221 () Real)
(declare-fun x_222 () Real)
(declare-fun x_223 () Real)
(declare-fun x_224 () Real)
(declare-fun x_225 () Bool)
(declare-fun x_226 () Bool)
(declare-fun x_227 () Real)
(declare-fun x_228 () Bool)
(declare-fun x_229 () Bool)
(declare-fun x_230 () Bool)
(declare-fun x_231 () Bool)
(declare-fun x_232 () Bool)
(declare-fun x_233 () Bool)
(declare-fun x_234 () Real)
(declare-fun x_235 () Bool)
(declare-fun x_236 () Bool)
(declare-fun x_237 () Real)
(declare-fun x_238 () Real)
(declare-fun x_239 () Real)
(declare-fun x_240 () Real)
(declare-fun x_241 () Real)
(declare-fun x_242 () Real)
(declare-fun x_243 () Bool)
(declare-fun x_244 () Bool)
(declare-fun x_245 () Real)
(declare-fun x_246 () Bool)
(declare-fun x_247 () Bool)
(declare-fun x_248 () Bool)
(declare-fun x_249 () Bool)
(declare-fun x_250 () Bool)
(declare-fun x_251 () Bool)
(declare-fun x_252 () Real)
(declare-fun x_253 () Bool)
(declare-fun x_254 () Bool)
(declare-fun x_255 () Real)
(declare-fun x_256 () Real)
(declare-fun x_257 () Real)
(declare-fun x_258 () Real)
(declare-fun x_259 () Real)
(assert (let ((?v_32 (+ x_227 x_18)) (?v_23 (+ x_237 x_18)) (?v_26 (= x_242 x_224)) (?v_2 (not x_243))) (let ((?v_4 (and ?v_2 x_244)) (?v_31 (= x_245 x_227)) (?v_24 (and (= x_246 x_228) (= x_247 x_229))) (?v_9 (= x_238 1)) (?v_33 (and (= x_248 x_230) (= x_249 x_231))) (?v_12 (and (= x_250 x_232) (= x_251 x_233))) (?v_5 (= x_252 x_234)) (?v_14 (not x_253))) (let ((?v_16 (and ?v_14 x_254)) (?v_17 (= x_255 0)) (?v_21 (= x_255 x_237)) (?v_0 (= x_238 0)) (?v_11 (+ x_234 x_18)) (?v_28 (= x_245 0)) (?v_60 (+ x_209 x_17)) (?v_53 (+ x_219 x_17)) (?v_56 (= x_224 x_206)) (?v_36 (not x_225))) (let ((?v_38 (and ?v_36 x_226)) (?v_59 (= x_227 x_209)) (?v_54 (and (= x_228 x_210) (= x_229 x_211))) (?v_41 (= x_220 1)) (?v_61 (and (= x_230 x_212) (= x_231 x_213))) (?v_44 (and (= x_232 x_214) (= x_233 x_215))) (?v_39 (= x_234 x_216)) (?v_46 (not x_235))) (let ((?v_48 (and ?v_46 x_236)) (?v_49 (= x_237 0)) (?v_51 (= x_237 x_219)) (?v_34 (= x_220 0)) (?v_43 (+ x_216 x_17)) (?v_58 (= x_227 0)) (?v_88 (+ x_191 x_16)) (?v_81 (+ x_201 x_16)) (?v_84 (= x_206 x_188)) (?v_64 (not x_207))) (let ((?v_66 (and ?v_64 x_208)) (?v_87 (= x_209 x_191)) (?v_82 (and (= x_210 x_192) (= x_211 x_193))) (?v_69 (= x_202 1)) (?v_89 (and (= x_212 x_194) (= x_213 x_195))) (?v_72 (and (= x_214 x_196) (= x_215 x_197))) (?v_67 (= x_216 x_198)) (?v_74 (not x_217))) (let ((?v_76 (and ?v_74 x_218)) (?v_77 (= x_219 0)) (?v_79 (= x_219 x_201)) (?v_62 (= x_202 0)) (?v_71 (+ x_198 x_16)) (?v_86 (= x_209 0)) (?v_116 (+ x_173 x_15)) (?v_109 (+ x_183 x_15)) (?v_112 (= x_188 x_170)) (?v_92 (not x_189))) (let ((?v_94 (and ?v_92 x_190)) (?v_115 (= x_191 x_173)) (?v_110 (and (= x_192 x_174) (= x_193 x_175))) (?v_97 (= x_184 1)) (?v_117 (and (= x_194 x_176) (= x_195 x_177))) (?v_100 (and (= x_196 x_178) (= x_197 x_179))) (?v_95 (= x_198 x_180)) (?v_102 (not x_199))) (let ((?v_104 (and ?v_102 x_200)) (?v_105 (= x_201 0)) (?v_107 (= x_201 x_183)) (?v_90 (= x_184 0)) (?v_99 (+ x_180 x_15)) (?v_114 (= x_191 0)) (?v_144 (+ x_155 x_14)) (?v_137 (+ x_165 x_14)) (?v_140 (= x_170 x_152)) (?v_120 (not x_171))) (let ((?v_122 (and ?v_120 x_172)) (?v_143 (= x_173 x_155)) (?v_138 (and (= x_174 x_156) (= x_175 x_157))) (?v_125 (= x_166 1)) (?v_145 (and (= x_176 x_158) (= x_177 x_159))) (?v_128 (and (= x_178 x_160) (= x_179 x_161))) (?v_123 (= x_180 x_162)) (?v_130 (not x_181))) (let ((?v_132 (and ?v_130 x_182)) (?v_133 (= x_183 0)) (?v_135 (= x_183 x_165)) (?v_118 (= x_166 0)) (?v_127 (+ x_162 x_14)) (?v_142 (= x_173 0)) (?v_172 (+ x_137 x_13)) (?v_165 (+ x_147 x_13)) (?v_168 (= x_152 x_134)) (?v_148 (not x_153))) (let ((?v_150 (and ?v_148 x_154)) (?v_171 (= x_155 x_137)) (?v_166 (and (= x_156 x_138) (= x_157 x_139))) (?v_153 (= x_148 1)) (?v_173 (and (= x_158 x_140) (= x_159 x_141))) (?v_156 (and (= x_160 x_142) (= x_161 x_143))) (?v_151 (= x_162 x_144)) (?v_158 (not x_163))) (let ((?v_160 (and ?v_158 x_164)) (?v_161 (= x_165 0)) (?v_163 (= x_165 x_147)) (?v_146 (= x_148 0)) (?v_155 (+ x_144 x_13)) (?v_170 (= x_155 0)) (?v_200 (+ x_119 x_12)) (?v_193 (+ x_129 x_12)) (?v_196 (= x_134 x_116)) (?v_176 (not x_135))) (let ((?v_178 (and ?v_176 x_136)) (?v_199 (= x_137 x_119)) (?v_194 (and (= x_138 x_120) (= x_139 x_121))) (?v_181 (= x_130 1)) (?v_201 (and (= x_140 x_122) (= x_141 x_123))) (?v_184 (and (= x_142 x_124) (= x_143 x_125))) (?v_179 (= x_144 x_126)) (?v_186 (not x_145))) (let ((?v_188 (and ?v_186 x_146)) (?v_189 (= x_147 0)) (?v_191 (= x_147 x_129)) (?v_174 (= x_130 0)) (?v_183 (+ x_126 x_12)) (?v_198 (= x_137 0)) (?v_228 (+ x_101 x_11)) (?v_221 (+ x_111 x_11)) (?v_224 (= x_116 x_98)) (?v_204 (not x_117))) (let ((?v_206 (and ?v_204 x_118)) (?v_227 (= x_119 x_101)) (?v_222 (and (= x_120 x_102) (= x_121 x_103))) (?v_209 (= x_112 1)) (?v_229 (and (= x_122 x_104) (= x_123 x_105))) (?v_212 (and (= x_124 x_106) (= x_125 x_107))) (?v_207 (= x_126 x_108)) (?v_214 (not x_127))) (let ((?v_216 (and ?v_214 x_128)) (?v_217 (= x_129 0)) (?v_219 (= x_129 x_111)) (?v_202 (= x_112 0)) (?v_211 (+ x_108 x_11)) (?v_226 (= x_119 0)) (?v_256 (+ x_83 x_10)) (?v_249 (+ x_93 x_10)) (?v_252 (= x_98 x_80)) (?v_232 (not x_99))) (let ((?v_234 (and ?v_232 x_100)) (?v_255 (= x_101 x_83)) (?v_250 (and (= x_102 x_84) (= x_103 x_85))) (?v_237 (= x_94 1)) (?v_257 (and (= x_104 x_86) (= x_105 x_87))) (?v_240 (and (= x_106 x_88) (= x_107 x_89))) (?v_235 (= x_108 x_90)) (?v_242 (not x_109))) (let ((?v_244 (and ?v_242 x_110)) (?v_245 (= x_111 0)) (?v_247 (= x_111 x_93)) (?v_230 (= x_94 0)) (?v_239 (+ x_90 x_10)) (?v_254 (= x_101 0)) (?v_284 (+ x_65 x_9)) (?v_277 (+ x_75 x_9)) (?v_280 (= x_80 x_62)) (?v_260 (not x_81))) (let ((?v_262 (and ?v_260 x_82)) (?v_283 (= x_83 x_65)) (?v_278 (and (= x_84 x_66) (= x_85 x_67))) (?v_265 (= x_76 1)) (?v_285 (and (= x_86 x_68) (= x_87 x_69))) (?v_268 (and (= x_88 x_70) (= x_89 x_71))) (?v_263 (= x_90 x_72)) (?v_270 (not x_91))) (let ((?v_272 (and ?v_270 x_92)) (?v_273 (= x_93 0)) (?v_275 (= x_93 x_75)) (?v_258 (= x_76 0)) (?v_267 (+ x_72 x_9)) (?v_282 (= x_83 0)) (?v_312 (+ x_47 x_8)) (?v_305 (+ x_57 x_8)) (?v_308 (= x_62 x_44)) (?v_288 (not x_63))) (let ((?v_290 (and ?v_288 x_64)) (?v_311 (= x_65 x_47)) (?v_306 (and (= x_66 x_48) (= x_67 x_49))) (?v_293 (= x_58 1)) (?v_313 (and (= x_68 x_50) (= x_69 x_51))) (?v_296 (and (= x_70 x_52) (= x_71 x_53))) (?v_291 (= x_72 x_54)) (?v_298 (not x_73))) (let ((?v_300 (and ?v_298 x_74)) (?v_301 (= x_75 0)) (?v_303 (= x_75 x_57)) (?v_286 (= x_58 0)) (?v_295 (+ x_54 x_8)) (?v_310 (= x_65 0)) (?v_340 (+ x_24 x_7)) (?v_333 (+ x_35 x_7)) (?v_336 (= x_44 x_20)) (?v_316 (not x_45))) (let ((?v_318 (and ?v_316 x_46)) (?v_339 (= x_47 x_24)) (?v_334 (and (= x_48 x_25) (= x_49 x_26))) (?v_321 (= x_36 1)) (?v_341 (and (= x_50 x_28) (= x_51 x_29))) (?v_324 (and (= x_52 x_30) (= x_53 x_31))) (?v_319 (= x_54 x_32)) (?v_326 (not x_55))) (let ((?v_328 (and ?v_326 x_56)) (?v_329 (= x_57 0)) (?v_331 (= x_57 x_35)) (?v_314 (= x_36 0)) (?v_323 (+ x_32 x_7)) (?v_338 (= x_47 0)) (?v_350 (+ 0 x_6)) (?v_362 (= x_20 x_21)) (?v_345 (not x_22))) (let ((?v_347 (and ?v_345 x_23)) (?v_363 (= x_24 0)) (?v_359 (and (= x_25 x_2) (= x_26 x_3))) (?v_364 (and (= x_28 x_4) (= x_29 x_5))) (?v_351 (and (= x_30 x_0) (= x_31 x_1))) (?v_346 (= x_32 0)) (?v_354 (not x_33))) (let ((?v_356 (and ?v_354 x_34)) (?v_355 (= x_35 0)) (?v_344 (not x_27)) (?v_342 (not x_0)) (?v_343 (not x_1)) (?v_352 (not x_2)) (?v_353 (not x_3)) (?v_360 (not x_4)) (?v_361 (not x_5)) (?v_3 (not x_232)) (?v_1 (not x_233)) (?v_6 (not x_244)) (?v_8 (not x_251)) (?v_7 (not x_250)) (?v_15 (not x_228)) (?v_13 (not x_229)) (?v_20 (not x_247)) (?v_18 (not x_254)) (?v_19 (not x_246)) (?v_27 (not x_230)) (?v_25 (not x_231)) (?v_30 (not x_249)) (?v_29 (not x_248)) (?v_37 (not x_214)) (?v_35 (not x_215)) (?v_40 (not x_226)) (?v_47 (not x_210)) (?v_45 (not x_211)) (?v_50 (not x_236)) (?v_57 (not x_212)) (?v_55 (not x_213)) (?v_65 (not x_196)) (?v_63 (not x_197)) (?v_68 (not x_208)) (?v_75 (not x_192)) (?v_73 (not x_193)) (?v_78 (not x_218)) (?v_85 (not x_194)) (?v_83 (not x_195)) (?v_93 (not x_178)) (?v_91 (not x_179)) (?v_96 (not x_190)) (?v_103 (not x_174)) (?v_101 (not x_175)) (?v_106 (not x_200)) (?v_113 (not x_176)) (?v_111 (not x_177)) (?v_121 (not x_160)) (?v_119 (not x_161)) (?v_124 (not x_172)) (?v_131 (not x_156)) (?v_129 (not x_157)) (?v_134 (not x_182)) (?v_141 (not x_158)) (?v_139 (not x_159)) (?v_149 (not x_142)) (?v_147 (not x_143)) (?v_152 (not x_154)) (?v_159 (not x_138)) (?v_157 (not x_139)) (?v_162 (not x_164)) (?v_169 (not x_140)) (?v_167 (not x_141)) (?v_177 (not x_124)) (?v_175 (not x_125)) (?v_180 (not x_136)) (?v_187 (not x_120)) (?v_185 (not x_121)) (?v_190 (not x_146)) (?v_197 (not x_122)) (?v_195 (not x_123)) (?v_205 (not x_106)) (?v_203 (not x_107)) (?v_208 (not x_118)) (?v_215 (not x_102)) (?v_213 (not x_103)) (?v_218 (not x_128)) (?v_225 (not x_104)) (?v_223 (not x_105)) (?v_233 (not x_88)) (?v_231 (not x_89)) (?v_236 (not x_100)) (?v_243 (not x_84)) (?v_241 (not x_85)) (?v_246 (not x_110)) (?v_253 (not x_86)) (?v_251 (not x_87)) (?v_261 (not x_70)) (?v_259 (not x_71)) (?v_264 (not x_82)) (?v_271 (not x_66)) (?v_269 (not x_67)) (?v_274 (not x_92)) (?v_281 (not x_68)) (?v_279 (not x_69)) (?v_289 (not x_52)) (?v_287 (not x_53)) (?v_292 (not x_64)) (?v_299 (not x_48)) (?v_297 (not x_49)) (?v_302 (not x_74)) (?v_309 (not x_50)) (?v_307 (not x_51)) (?v_317 (not x_30)) (?v_315 (not x_31)) (?v_320 (not x_46)) (?v_327 (not x_25)) (?v_325 (not x_26)) (?v_330 (not x_56)) (?v_337 (not x_28)) (?v_335 (not x_29)) (?v_348 (not x_23)) (?v_357 (not x_34)) (?v_10 (<= ?v_11 5)) (?v_22 (<= ?v_23 1)) (?v_42 (<= ?v_43 5)) (?v_52 (<= ?v_53 1)) (?v_70 (<= ?v_71 5)) (?v_80 (<= ?v_81 1)) (?v_98 (<= ?v_99 5)) (?v_108 (<= ?v_109 1)) (?v_126 (<= ?v_127 5)) (?v_136 (<= ?v_137 1)) (?v_154 (<= ?v_155 5)) (?v_164 (<= ?v_165 1)) (?v_182 (<= ?v_183 5)) (?v_192 (<= ?v_193 1)) (?v_210 (<= ?v_211 5)) (?v_220 (<= ?v_221 1)) (?v_238 (<= ?v_239 5)) (?v_248 (<= ?v_249 1)) (?v_266 (<= ?v_267 5)) (?v_276 (<= ?v_277 1)) (?v_294 (<= ?v_295 5)) (?v_304 (<= ?v_305 1)) (?v_322 (<= ?v_323 5)) (?v_332 (<= ?v_333 1)) (?v_349 (<= ?v_350 5)) (?v_358 (<= ?v_350 1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_256 1) (>= x_256 0)) (<= x_238 1)) (>= x_238 0)) (<= x_220 1)) (>= x_220 0)) (<= x_202 1)) (>= x_202 0)) (<= x_184 1)) (>= x_184 0)) (<= x_166 1)) (>= x_166 0)) (<= x_148 1)) (>= x_148 0)) (<= x_130 1)) (>= x_130 0)) (<= x_112 1)) (>= x_112 0)) (<= x_94 1)) (>= x_94 0)) (<= x_76 1)) (>= x_76 0)) (<= x_58 1)) (>= x_58 0)) (<= x_36 1)) (>= x_36 0)) (and ?v_342 ?v_343)) (and ?v_352 ?v_353)) (and ?v_360 ?v_361)) (not (< x_19 0))) (not (< x_18 0))) (not (< x_17 0))) (not (< x_16 0))) (not (< x_15 0))) (not (< x_14 0))) (not (< x_13 0))) (not (< x_12 0))) (not (< x_11 0))) (not (< x_10 0))) (not (< x_9 0))) (not (< x_8 0))) (not (< x_7 0))) (not (< x_6 0))) (= x_256 (ite ?v_9 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_257 0) ?v_0) ?v_3) ?v_1) ?v_2) ?v_6) x_250) ?v_8) (= x_252 0)) (and (and (and (and (and (and (and (and (= x_257 1) ?v_0) x_232) ?v_1) (not (<= x_234 2))) ?v_4) ?v_7) x_251) ?v_5)) (and (and (and (and (and (and (and (= x_257 2) ?v_0) ?v_3) x_233) ?v_4) x_250) x_251) ?v_5)) (and (and (and (and (and (and (and (and (= x_257 3) ?v_0) x_232) x_233) x_243) ?v_6) ?v_7) ?v_8) ?v_5)) (and (and (and (and (and (and (and (and (= x_257 4) ?v_9) (or (or ?v_3 x_233) ?v_10)) (or (or x_232 ?v_1) ?v_10)) (or (or ?v_3 ?v_1) ?v_10)) (= x_252 ?v_11)) (= x_243 x_225)) (= x_244 x_226)) ?v_12)) (and (and (and (and (= x_257 5) ?v_0) ?v_5) ?v_4) ?v_12))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_258 0) ?v_0) ?v_15) ?v_13) ?v_2) ?v_6) ?v_16) x_246) ?v_20) ?v_17) (and (and (and (and (and (and (and (and (and (= x_258 1) ?v_0) x_228) ?v_13) (= x_237 1)) ?v_14) ?v_18) ?v_19) x_247) ?v_21)) (and (and (and (and (and (and (and (and (and (= x_258 2) ?v_0) ?v_15) x_229) x_243) ?v_6) ?v_16) x_246) x_247) ?v_17)) (and (and (and (and (and (and (and (and (= x_258 3) ?v_0) x_228) x_229) x_253) ?v_18) ?v_19) ?v_20) ?v_21)) (and (and (and (and (and (and (and (= x_258 4) ?v_9) (or (or ?v_15 x_229) ?v_22)) (or (or ?v_15 ?v_13) ?v_22)) (= x_255 ?v_23)) (= x_253 x_235)) (= x_254 x_236)) ?v_24)) (and (and (and (and (and (and (= x_258 5) ?v_0) ?v_2) x_244) ?v_21) ?v_16) ?v_24))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_259 0) ?v_0) ?v_27) ?v_25) ?v_14) ?v_18) x_248) ?v_30) ?v_28) ?v_26) (and (and (and (and (and (and (and (= x_259 1) ?v_0) x_230) ?v_25) ?v_29) x_249) ?v_26) ?v_31)) (and (and (and (and (and (and (and (and (and (= x_259 2) ?v_0) ?v_27) x_231) x_253) ?v_18) x_248) x_249) ?v_28) ?v_26)) (and (and (and (and (and (and (and (and (= x_259 3) ?v_0) x_230) x_231) (not (< x_227 1))) ?v_29) ?v_30) ?v_26) ?v_31)) (and (and (and (and (and (and (= x_259 4) ?v_9) (or (or ?v_27 x_231) (<= ?v_32 1))) (or (or ?v_27 ?v_25) (<= ?v_32 2))) (= x_245 ?v_32)) ?v_33) ?v_26)) (and (and (and (and (and (and (= x_259 5) ?v_0) ?v_14) x_254) ?v_31) ?v_33) ?v_26))) (= x_238 (ite ?v_41 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_239 0) ?v_34) ?v_37) ?v_35) ?v_36) ?v_40) x_232) ?v_1) (= x_234 0)) (and (and (and (and (and (and (and (and (= x_239 1) ?v_34) x_214) ?v_35) (not (<= x_216 2))) ?v_38) ?v_3) x_233) ?v_39)) (and (and (and (and (and (and (and (= x_239 2) ?v_34) ?v_37) x_215) ?v_38) x_232) x_233) ?v_39)) (and (and (and (and (and (and (and (and (= x_239 3) ?v_34) x_214) x_215) x_225) ?v_40) ?v_3) ?v_1) ?v_39)) (and (and (and (and (and (and (and (and (= x_239 4) ?v_41) (or (or ?v_37 x_215) ?v_42)) (or (or x_214 ?v_35) ?v_42)) (or (or ?v_37 ?v_35) ?v_42)) (= x_234 ?v_43)) (= x_225 x_207)) (= x_226 x_208)) ?v_44)) (and (and (and (and (= x_239 5) ?v_34) ?v_39) ?v_38) ?v_44))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_240 0) ?v_34) ?v_47) ?v_45) ?v_36) ?v_40) ?v_48) x_228) ?v_13) ?v_49) (and (and (and (and (and (and (and (and (and (= x_240 1) ?v_34) x_210) ?v_45) (= x_219 1)) ?v_46) ?v_50) ?v_15) x_229) ?v_51)) (and (and (and (and (and (and (and (and (and (= x_240 2) ?v_34) ?v_47) x_211) x_225) ?v_40) ?v_48) x_228) x_229) ?v_49)) (and (and (and (and (and (and (and (and (= x_240 3) ?v_34) x_210) x_211) x_235) ?v_50) ?v_15) ?v_13) ?v_51)) (and (and (and (and (and (and (and (= x_240 4) ?v_41) (or (or ?v_47 x_211) ?v_52)) (or (or ?v_47 ?v_45) ?v_52)) (= x_237 ?v_53)) (= x_235 x_217)) (= x_236 x_218)) ?v_54)) (and (and (and (and (and (and (= x_240 5) ?v_34) ?v_36) x_226) ?v_51) ?v_48) ?v_54))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_241 0) ?v_34) ?v_57) ?v_55) ?v_46) ?v_50) x_230) ?v_25) ?v_58) ?v_56) (and (and (and (and (and (and (and (= x_241 1) ?v_34) x_212) ?v_55) ?v_27) x_231) ?v_56) ?v_59)) (and (and (and (and (and (and (and (and (and (= x_241 2) ?v_34) ?v_57) x_213) x_235) ?v_50) x_230) x_231) ?v_58) ?v_56)) (and (and (and (and (and (and (and (and (= x_241 3) ?v_34) x_212) x_213) (not (< x_209 1))) ?v_27) ?v_25) ?v_56) ?v_59)) (and (and (and (and (and (and (= x_241 4) ?v_41) (or (or ?v_57 x_213) (<= ?v_60 1))) (or (or ?v_57 ?v_55) (<= ?v_60 2))) (= x_227 ?v_60)) ?v_61) ?v_56)) (and (and (and (and (and (and (= x_241 5) ?v_34) ?v_46) x_236) ?v_59) ?v_61) ?v_56))) (= x_220 (ite ?v_69 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_221 0) ?v_62) ?v_65) ?v_63) ?v_64) ?v_68) x_214) ?v_35) (= x_216 0)) (and (and (and (and (and (and (and (and (= x_221 1) ?v_62) x_196) ?v_63) (not (<= x_198 2))) ?v_66) ?v_37) x_215) ?v_67)) (and (and (and (and (and (and (and (= x_221 2) ?v_62) ?v_65) x_197) ?v_66) x_214) x_215) ?v_67)) (and (and (and (and (and (and (and (and (= x_221 3) ?v_62) x_196) x_197) x_207) ?v_68) ?v_37) ?v_35) ?v_67)) (and (and (and (and (and (and (and (and (= x_221 4) ?v_69) (or (or ?v_65 x_197) ?v_70)) (or (or x_196 ?v_63) ?v_70)) (or (or ?v_65 ?v_63) ?v_70)) (= x_216 ?v_71)) (= x_207 x_189)) (= x_208 x_190)) ?v_72)) (and (and (and (and (= x_221 5) ?v_62) ?v_67) ?v_66) ?v_72))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_222 0) ?v_62) ?v_75) ?v_73) ?v_64) ?v_68) ?v_76) x_210) ?v_45) ?v_77) (and (and (and (and (and (and (and (and (and (= x_222 1) ?v_62) x_192) ?v_73) (= x_201 1)) ?v_74) ?v_78) ?v_47) x_211) ?v_79)) (and (and (and (and (and (and (and (and (and (= x_222 2) ?v_62) ?v_75) x_193) x_207) ?v_68) ?v_76) x_210) x_211) ?v_77)) (and (and (and (and (and (and (and (and (= x_222 3) ?v_62) x_192) x_193) x_217) ?v_78) ?v_47) ?v_45) ?v_79)) (and (and (and (and (and (and (and (= x_222 4) ?v_69) (or (or ?v_75 x_193) ?v_80)) (or (or ?v_75 ?v_73) ?v_80)) (= x_219 ?v_81)) (= x_217 x_199)) (= x_218 x_200)) ?v_82)) (and (and (and (and (and (and (= x_222 5) ?v_62) ?v_64) x_208) ?v_79) ?v_76) ?v_82))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_223 0) ?v_62) ?v_85) ?v_83) ?v_74) ?v_78) x_212) ?v_55) ?v_86) ?v_84) (and (and (and (and (and (and (and (= x_223 1) ?v_62) x_194) ?v_83) ?v_57) x_213) ?v_84) ?v_87)) (and (and (and (and (and (and (and (and (and (= x_223 2) ?v_62) ?v_85) x_195) x_217) ?v_78) x_212) x_213) ?v_86) ?v_84)) (and (and (and (and (and (and (and (and (= x_223 3) ?v_62) x_194) x_195) (not (< x_191 1))) ?v_57) ?v_55) ?v_84) ?v_87)) (and (and (and (and (and (and (= x_223 4) ?v_69) (or (or ?v_85 x_195) (<= ?v_88 1))) (or (or ?v_85 ?v_83) (<= ?v_88 2))) (= x_209 ?v_88)) ?v_89) ?v_84)) (and (and (and (and (and (and (= x_223 5) ?v_62) ?v_74) x_218) ?v_87) ?v_89) ?v_84))) (= x_202 (ite ?v_97 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_203 0) ?v_90) ?v_93) ?v_91) ?v_92) ?v_96) x_196) ?v_63) (= x_198 0)) (and (and (and (and (and (and (and (and (= x_203 1) ?v_90) x_178) ?v_91) (not (<= x_180 2))) ?v_94) ?v_65) x_197) ?v_95)) (and (and (and (and (and (and (and (= x_203 2) ?v_90) ?v_93) x_179) ?v_94) x_196) x_197) ?v_95)) (and (and (and (and (and (and (and (and (= x_203 3) ?v_90) x_178) x_179) x_189) ?v_96) ?v_65) ?v_63) ?v_95)) (and (and (and (and (and (and (and (and (= x_203 4) ?v_97) (or (or ?v_93 x_179) ?v_98)) (or (or x_178 ?v_91) ?v_98)) (or (or ?v_93 ?v_91) ?v_98)) (= x_198 ?v_99)) (= x_189 x_171)) (= x_190 x_172)) ?v_100)) (and (and (and (and (= x_203 5) ?v_90) ?v_95) ?v_94) ?v_100))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_204 0) ?v_90) ?v_103) ?v_101) ?v_92) ?v_96) ?v_104) x_192) ?v_73) ?v_105) (and (and (and (and (and (and (and (and (and (= x_204 1) ?v_90) x_174) ?v_101) (= x_183 1)) ?v_102) ?v_106) ?v_75) x_193) ?v_107)) (and (and (and (and (and (and (and (and (and (= x_204 2) ?v_90) ?v_103) x_175) x_189) ?v_96) ?v_104) x_192) x_193) ?v_105)) (and (and (and (and (and (and (and (and (= x_204 3) ?v_90) x_174) x_175) x_199) ?v_106) ?v_75) ?v_73) ?v_107)) (and (and (and (and (and (and (and (= x_204 4) ?v_97) (or (or ?v_103 x_175) ?v_108)) (or (or ?v_103 ?v_101) ?v_108)) (= x_201 ?v_109)) (= x_199 x_181)) (= x_200 x_182)) ?v_110)) (and (and (and (and (and (and (= x_204 5) ?v_90) ?v_92) x_190) ?v_107) ?v_104) ?v_110))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_205 0) ?v_90) ?v_113) ?v_111) ?v_102) ?v_106) x_194) ?v_83) ?v_114) ?v_112) (and (and (and (and (and (and (and (= x_205 1) ?v_90) x_176) ?v_111) ?v_85) x_195) ?v_112) ?v_115)) (and (and (and (and (and (and (and (and (and (= x_205 2) ?v_90) ?v_113) x_177) x_199) ?v_106) x_194) x_195) ?v_114) ?v_112)) (and (and (and (and (and (and (and (and (= x_205 3) ?v_90) x_176) x_177) (not (< x_173 1))) ?v_85) ?v_83) ?v_112) ?v_115)) (and (and (and (and (and (and (= x_205 4) ?v_97) (or (or ?v_113 x_177) (<= ?v_116 1))) (or (or ?v_113 ?v_111) (<= ?v_116 2))) (= x_191 ?v_116)) ?v_117) ?v_112)) (and (and (and (and (and (and (= x_205 5) ?v_90) ?v_102) x_200) ?v_115) ?v_117) ?v_112))) (= x_184 (ite ?v_125 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_185 0) ?v_118) ?v_121) ?v_119) ?v_120) ?v_124) x_178) ?v_91) (= x_180 0)) (and (and (and (and (and (and (and (and (= x_185 1) ?v_118) x_160) ?v_119) (not (<= x_162 2))) ?v_122) ?v_93) x_179) ?v_123)) (and (and (and (and (and (and (and (= x_185 2) ?v_118) ?v_121) x_161) ?v_122) x_178) x_179) ?v_123)) (and (and (and (and (and (and (and (and (= x_185 3) ?v_118) x_160) x_161) x_171) ?v_124) ?v_93) ?v_91) ?v_123)) (and (and (and (and (and (and (and (and (= x_185 4) ?v_125) (or (or ?v_121 x_161) ?v_126)) (or (or x_160 ?v_119) ?v_126)) (or (or ?v_121 ?v_119) ?v_126)) (= x_180 ?v_127)) (= x_171 x_153)) (= x_172 x_154)) ?v_128)) (and (and (and (and (= x_185 5) ?v_118) ?v_123) ?v_122) ?v_128))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_186 0) ?v_118) ?v_131) ?v_129) ?v_120) ?v_124) ?v_132) x_174) ?v_101) ?v_133) (and (and (and (and (and (and (and (and (and (= x_186 1) ?v_118) x_156) ?v_129) (= x_165 1)) ?v_130) ?v_134) ?v_103) x_175) ?v_135)) (and (and (and (and (and (and (and (and (and (= x_186 2) ?v_118) ?v_131) x_157) x_171) ?v_124) ?v_132) x_174) x_175) ?v_133)) (and (and (and (and (and (and (and (and (= x_186 3) ?v_118) x_156) x_157) x_181) ?v_134) ?v_103) ?v_101) ?v_135)) (and (and (and (and (and (and (and (= x_186 4) ?v_125) (or (or ?v_131 x_157) ?v_136)) (or (or ?v_131 ?v_129) ?v_136)) (= x_183 ?v_137)) (= x_181 x_163)) (= x_182 x_164)) ?v_138)) (and (and (and (and (and (and (= x_186 5) ?v_118) ?v_120) x_172) ?v_135) ?v_132) ?v_138))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_187 0) ?v_118) ?v_141) ?v_139) ?v_130) ?v_134) x_176) ?v_111) ?v_142) ?v_140) (and (and (and (and (and (and (and (= x_187 1) ?v_118) x_158) ?v_139) ?v_113) x_177) ?v_140) ?v_143)) (and (and (and (and (and (and (and (and (and (= x_187 2) ?v_118) ?v_141) x_159) x_181) ?v_134) x_176) x_177) ?v_142) ?v_140)) (and (and (and (and (and (and (and (and (= x_187 3) ?v_118) x_158) x_159) (not (< x_155 1))) ?v_113) ?v_111) ?v_140) ?v_143)) (and (and (and (and (and (and (= x_187 4) ?v_125) (or (or ?v_141 x_159) (<= ?v_144 1))) (or (or ?v_141 ?v_139) (<= ?v_144 2))) (= x_173 ?v_144)) ?v_145) ?v_140)) (and (and (and (and (and (and (= x_187 5) ?v_118) ?v_130) x_182) ?v_143) ?v_145) ?v_140))) (= x_166 (ite ?v_153 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_167 0) ?v_146) ?v_149) ?v_147) ?v_148) ?v_152) x_160) ?v_119) (= x_162 0)) (and (and (and (and (and (and (and (and (= x_167 1) ?v_146) x_142) ?v_147) (not (<= x_144 2))) ?v_150) ?v_121) x_161) ?v_151)) (and (and (and (and (and (and (and (= x_167 2) ?v_146) ?v_149) x_143) ?v_150) x_160) x_161) ?v_151)) (and (and (and (and (and (and (and (and (= x_167 3) ?v_146) x_142) x_143) x_153) ?v_152) ?v_121) ?v_119) ?v_151)) (and (and (and (and (and (and (and (and (= x_167 4) ?v_153) (or (or ?v_149 x_143) ?v_154)) (or (or x_142 ?v_147) ?v_154)) (or (or ?v_149 ?v_147) ?v_154)) (= x_162 ?v_155)) (= x_153 x_135)) (= x_154 x_136)) ?v_156)) (and (and (and (and (= x_167 5) ?v_146) ?v_151) ?v_150) ?v_156))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_168 0) ?v_146) ?v_159) ?v_157) ?v_148) ?v_152) ?v_160) x_156) ?v_129) ?v_161) (and (and (and (and (and (and (and (and (and (= x_168 1) ?v_146) x_138) ?v_157) (= x_147 1)) ?v_158) ?v_162) ?v_131) x_157) ?v_163)) (and (and (and (and (and (and (and (and (and (= x_168 2) ?v_146) ?v_159) x_139) x_153) ?v_152) ?v_160) x_156) x_157) ?v_161)) (and (and (and (and (and (and (and (and (= x_168 3) ?v_146) x_138) x_139) x_163) ?v_162) ?v_131) ?v_129) ?v_163)) (and (and (and (and (and (and (and (= x_168 4) ?v_153) (or (or ?v_159 x_139) ?v_164)) (or (or ?v_159 ?v_157) ?v_164)) (= x_165 ?v_165)) (= x_163 x_145)) (= x_164 x_146)) ?v_166)) (and (and (and (and (and (and (= x_168 5) ?v_146) ?v_148) x_154) ?v_163) ?v_160) ?v_166))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_169 0) ?v_146) ?v_169) ?v_167) ?v_158) ?v_162) x_158) ?v_139) ?v_170) ?v_168) (and (and (and (and (and (and (and (= x_169 1) ?v_146) x_140) ?v_167) ?v_141) x_159) ?v_168) ?v_171)) (and (and (and (and (and (and (and (and (and (= x_169 2) ?v_146) ?v_169) x_141) x_163) ?v_162) x_158) x_159) ?v_170) ?v_168)) (and (and (and (and (and (and (and (and (= x_169 3) ?v_146) x_140) x_141) (not (< x_137 1))) ?v_141) ?v_139) ?v_168) ?v_171)) (and (and (and (and (and (and (= x_169 4) ?v_153) (or (or ?v_169 x_141) (<= ?v_172 1))) (or (or ?v_169 ?v_167) (<= ?v_172 2))) (= x_155 ?v_172)) ?v_173) ?v_168)) (and (and (and (and (and (and (= x_169 5) ?v_146) ?v_158) x_164) ?v_171) ?v_173) ?v_168))) (= x_148 (ite ?v_181 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_149 0) ?v_174) ?v_177) ?v_175) ?v_176) ?v_180) x_142) ?v_147) (= x_144 0)) (and (and (and (and (and (and (and (and (= x_149 1) ?v_174) x_124) ?v_175) (not (<= x_126 2))) ?v_178) ?v_149) x_143) ?v_179)) (and (and (and (and (and (and (and (= x_149 2) ?v_174) ?v_177) x_125) ?v_178) x_142) x_143) ?v_179)) (and (and (and (and (and (and (and (and (= x_149 3) ?v_174) x_124) x_125) x_135) ?v_180) ?v_149) ?v_147) ?v_179)) (and (and (and (and (and (and (and (and (= x_149 4) ?v_181) (or (or ?v_177 x_125) ?v_182)) (or (or x_124 ?v_175) ?v_182)) (or (or ?v_177 ?v_175) ?v_182)) (= x_144 ?v_183)) (= x_135 x_117)) (= x_136 x_118)) ?v_184)) (and (and (and (and (= x_149 5) ?v_174) ?v_179) ?v_178) ?v_184))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_150 0) ?v_174) ?v_187) ?v_185) ?v_176) ?v_180) ?v_188) x_138) ?v_157) ?v_189) (and (and (and (and (and (and (and (and (and (= x_150 1) ?v_174) x_120) ?v_185) (= x_129 1)) ?v_186) ?v_190) ?v_159) x_139) ?v_191)) (and (and (and (and (and (and (and (and (and (= x_150 2) ?v_174) ?v_187) x_121) x_135) ?v_180) ?v_188) x_138) x_139) ?v_189)) (and (and (and (and (and (and (and (and (= x_150 3) ?v_174) x_120) x_121) x_145) ?v_190) ?v_159) ?v_157) ?v_191)) (and (and (and (and (and (and (and (= x_150 4) ?v_181) (or (or ?v_187 x_121) ?v_192)) (or (or ?v_187 ?v_185) ?v_192)) (= x_147 ?v_193)) (= x_145 x_127)) (= x_146 x_128)) ?v_194)) (and (and (and (and (and (and (= x_150 5) ?v_174) ?v_176) x_136) ?v_191) ?v_188) ?v_194))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_151 0) ?v_174) ?v_197) ?v_195) ?v_186) ?v_190) x_140) ?v_167) ?v_198) ?v_196) (and (and (and (and (and (and (and (= x_151 1) ?v_174) x_122) ?v_195) ?v_169) x_141) ?v_196) ?v_199)) (and (and (and (and (and (and (and (and (and (= x_151 2) ?v_174) ?v_197) x_123) x_145) ?v_190) x_140) x_141) ?v_198) ?v_196)) (and (and (and (and (and (and (and (and (= x_151 3) ?v_174) x_122) x_123) (not (< x_119 1))) ?v_169) ?v_167) ?v_196) ?v_199)) (and (and (and (and (and (and (= x_151 4) ?v_181) (or (or ?v_197 x_123) (<= ?v_200 1))) (or (or ?v_197 ?v_195) (<= ?v_200 2))) (= x_137 ?v_200)) ?v_201) ?v_196)) (and (and (and (and (and (and (= x_151 5) ?v_174) ?v_186) x_146) ?v_199) ?v_201) ?v_196))) (= x_130 (ite ?v_209 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_131 0) ?v_202) ?v_205) ?v_203) ?v_204) ?v_208) x_124) ?v_175) (= x_126 0)) (and (and (and (and (and (and (and (and (= x_131 1) ?v_202) x_106) ?v_203) (not (<= x_108 2))) ?v_206) ?v_177) x_125) ?v_207)) (and (and (and (and (and (and (and (= x_131 2) ?v_202) ?v_205) x_107) ?v_206) x_124) x_125) ?v_207)) (and (and (and (and (and (and (and (and (= x_131 3) ?v_202) x_106) x_107) x_117) ?v_208) ?v_177) ?v_175) ?v_207)) (and (and (and (and (and (and (and (and (= x_131 4) ?v_209) (or (or ?v_205 x_107) ?v_210)) (or (or x_106 ?v_203) ?v_210)) (or (or ?v_205 ?v_203) ?v_210)) (= x_126 ?v_211)) (= x_117 x_99)) (= x_118 x_100)) ?v_212)) (and (and (and (and (= x_131 5) ?v_202) ?v_207) ?v_206) ?v_212))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_132 0) ?v_202) ?v_215) ?v_213) ?v_204) ?v_208) ?v_216) x_120) ?v_185) ?v_217) (and (and (and (and (and (and (and (and (and (= x_132 1) ?v_202) x_102) ?v_213) (= x_111 1)) ?v_214) ?v_218) ?v_187) x_121) ?v_219)) (and (and (and (and (and (and (and (and (and (= x_132 2) ?v_202) ?v_215) x_103) x_117) ?v_208) ?v_216) x_120) x_121) ?v_217)) (and (and (and (and (and (and (and (and (= x_132 3) ?v_202) x_102) x_103) x_127) ?v_218) ?v_187) ?v_185) ?v_219)) (and (and (and (and (and (and (and (= x_132 4) ?v_209) (or (or ?v_215 x_103) ?v_220)) (or (or ?v_215 ?v_213) ?v_220)) (= x_129 ?v_221)) (= x_127 x_109)) (= x_128 x_110)) ?v_222)) (and (and (and (and (and (and (= x_132 5) ?v_202) ?v_204) x_118) ?v_219) ?v_216) ?v_222))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_133 0) ?v_202) ?v_225) ?v_223) ?v_214) ?v_218) x_122) ?v_195) ?v_226) ?v_224) (and (and (and (and (and (and (and (= x_133 1) ?v_202) x_104) ?v_223) ?v_197) x_123) ?v_224) ?v_227)) (and (and (and (and (and (and (and (and (and (= x_133 2) ?v_202) ?v_225) x_105) x_127) ?v_218) x_122) x_123) ?v_226) ?v_224)) (and (and (and (and (and (and (and (and (= x_133 3) ?v_202) x_104) x_105) (not (< x_101 1))) ?v_197) ?v_195) ?v_224) ?v_227)) (and (and (and (and (and (and (= x_133 4) ?v_209) (or (or ?v_225 x_105) (<= ?v_228 1))) (or (or ?v_225 ?v_223) (<= ?v_228 2))) (= x_119 ?v_228)) ?v_229) ?v_224)) (and (and (and (and (and (and (= x_133 5) ?v_202) ?v_214) x_128) ?v_227) ?v_229) ?v_224))) (= x_112 (ite ?v_237 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_113 0) ?v_230) ?v_233) ?v_231) ?v_232) ?v_236) x_106) ?v_203) (= x_108 0)) (and (and (and (and (and (and (and (and (= x_113 1) ?v_230) x_88) ?v_231) (not (<= x_90 2))) ?v_234) ?v_205) x_107) ?v_235)) (and (and (and (and (and (and (and (= x_113 2) ?v_230) ?v_233) x_89) ?v_234) x_106) x_107) ?v_235)) (and (and (and (and (and (and (and (and (= x_113 3) ?v_230) x_88) x_89) x_99) ?v_236) ?v_205) ?v_203) ?v_235)) (and (and (and (and (and (and (and (and (= x_113 4) ?v_237) (or (or ?v_233 x_89) ?v_238)) (or (or x_88 ?v_231) ?v_238)) (or (or ?v_233 ?v_231) ?v_238)) (= x_108 ?v_239)) (= x_99 x_81)) (= x_100 x_82)) ?v_240)) (and (and (and (and (= x_113 5) ?v_230) ?v_235) ?v_234) ?v_240))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_114 0) ?v_230) ?v_243) ?v_241) ?v_232) ?v_236) ?v_244) x_102) ?v_213) ?v_245) (and (and (and (and (and (and (and (and (and (= x_114 1) ?v_230) x_84) ?v_241) (= x_93 1)) ?v_242) ?v_246) ?v_215) x_103) ?v_247)) (and (and (and (and (and (and (and (and (and (= x_114 2) ?v_230) ?v_243) x_85) x_99) ?v_236) ?v_244) x_102) x_103) ?v_245)) (and (and (and (and (and (and (and (and (= x_114 3) ?v_230) x_84) x_85) x_109) ?v_246) ?v_215) ?v_213) ?v_247)) (and (and (and (and (and (and (and (= x_114 4) ?v_237) (or (or ?v_243 x_85) ?v_248)) (or (or ?v_243 ?v_241) ?v_248)) (= x_111 ?v_249)) (= x_109 x_91)) (= x_110 x_92)) ?v_250)) (and (and (and (and (and (and (= x_114 5) ?v_230) ?v_232) x_100) ?v_247) ?v_244) ?v_250))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_115 0) ?v_230) ?v_253) ?v_251) ?v_242) ?v_246) x_104) ?v_223) ?v_254) ?v_252) (and (and (and (and (and (and (and (= x_115 1) ?v_230) x_86) ?v_251) ?v_225) x_105) ?v_252) ?v_255)) (and (and (and (and (and (and (and (and (and (= x_115 2) ?v_230) ?v_253) x_87) x_109) ?v_246) x_104) x_105) ?v_254) ?v_252)) (and (and (and (and (and (and (and (and (= x_115 3) ?v_230) x_86) x_87) (not (< x_83 1))) ?v_225) ?v_223) ?v_252) ?v_255)) (and (and (and (and (and (and (= x_115 4) ?v_237) (or (or ?v_253 x_87) (<= ?v_256 1))) (or (or ?v_253 ?v_251) (<= ?v_256 2))) (= x_101 ?v_256)) ?v_257) ?v_252)) (and (and (and (and (and (and (= x_115 5) ?v_230) ?v_242) x_110) ?v_255) ?v_257) ?v_252))) (= x_94 (ite ?v_265 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_95 0) ?v_258) ?v_261) ?v_259) ?v_260) ?v_264) x_88) ?v_231) (= x_90 0)) (and (and (and (and (and (and (and (and (= x_95 1) ?v_258) x_70) ?v_259) (not (<= x_72 2))) ?v_262) ?v_233) x_89) ?v_263)) (and (and (and (and (and (and (and (= x_95 2) ?v_258) ?v_261) x_71) ?v_262) x_88) x_89) ?v_263)) (and (and (and (and (and (and (and (and (= x_95 3) ?v_258) x_70) x_71) x_81) ?v_264) ?v_233) ?v_231) ?v_263)) (and (and (and (and (and (and (and (and (= x_95 4) ?v_265) (or (or ?v_261 x_71) ?v_266)) (or (or x_70 ?v_259) ?v_266)) (or (or ?v_261 ?v_259) ?v_266)) (= x_90 ?v_267)) (= x_81 x_63)) (= x_82 x_64)) ?v_268)) (and (and (and (and (= x_95 5) ?v_258) ?v_263) ?v_262) ?v_268))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_96 0) ?v_258) ?v_271) ?v_269) ?v_260) ?v_264) ?v_272) x_84) ?v_241) ?v_273) (and (and (and (and (and (and (and (and (and (= x_96 1) ?v_258) x_66) ?v_269) (= x_75 1)) ?v_270) ?v_274) ?v_243) x_85) ?v_275)) (and (and (and (and (and (and (and (and (and (= x_96 2) ?v_258) ?v_271) x_67) x_81) ?v_264) ?v_272) x_84) x_85) ?v_273)) (and (and (and (and (and (and (and (and (= x_96 3) ?v_258) x_66) x_67) x_91) ?v_274) ?v_243) ?v_241) ?v_275)) (and (and (and (and (and (and (and (= x_96 4) ?v_265) (or (or ?v_271 x_67) ?v_276)) (or (or ?v_271 ?v_269) ?v_276)) (= x_93 ?v_277)) (= x_91 x_73)) (= x_92 x_74)) ?v_278)) (and (and (and (and (and (and (= x_96 5) ?v_258) ?v_260) x_82) ?v_275) ?v_272) ?v_278))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_97 0) ?v_258) ?v_281) ?v_279) ?v_270) ?v_274) x_86) ?v_251) ?v_282) ?v_280) (and (and (and (and (and (and (and (= x_97 1) ?v_258) x_68) ?v_279) ?v_253) x_87) ?v_280) ?v_283)) (and (and (and (and (and (and (and (and (and (= x_97 2) ?v_258) ?v_281) x_69) x_91) ?v_274) x_86) x_87) ?v_282) ?v_280)) (and (and (and (and (and (and (and (and (= x_97 3) ?v_258) x_68) x_69) (not (< x_65 1))) ?v_253) ?v_251) ?v_280) ?v_283)) (and (and (and (and (and (and (= x_97 4) ?v_265) (or (or ?v_281 x_69) (<= ?v_284 1))) (or (or ?v_281 ?v_279) (<= ?v_284 2))) (= x_83 ?v_284)) ?v_285) ?v_280)) (and (and (and (and (and (and (= x_97 5) ?v_258) ?v_270) x_92) ?v_283) ?v_285) ?v_280))) (= x_76 (ite ?v_293 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_77 0) ?v_286) ?v_289) ?v_287) ?v_288) ?v_292) x_70) ?v_259) (= x_72 0)) (and (and (and (and (and (and (and (and (= x_77 1) ?v_286) x_52) ?v_287) (not (<= x_54 2))) ?v_290) ?v_261) x_71) ?v_291)) (and (and (and (and (and (and (and (= x_77 2) ?v_286) ?v_289) x_53) ?v_290) x_70) x_71) ?v_291)) (and (and (and (and (and (and (and (and (= x_77 3) ?v_286) x_52) x_53) x_63) ?v_292) ?v_261) ?v_259) ?v_291)) (and (and (and (and (and (and (and (and (= x_77 4) ?v_293) (or (or ?v_289 x_53) ?v_294)) (or (or x_52 ?v_287) ?v_294)) (or (or ?v_289 ?v_287) ?v_294)) (= x_72 ?v_295)) (= x_63 x_45)) (= x_64 x_46)) ?v_296)) (and (and (and (and (= x_77 5) ?v_286) ?v_291) ?v_290) ?v_296))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_78 0) ?v_286) ?v_299) ?v_297) ?v_288) ?v_292) ?v_300) x_66) ?v_269) ?v_301) (and (and (and (and (and (and (and (and (and (= x_78 1) ?v_286) x_48) ?v_297) (= x_57 1)) ?v_298) ?v_302) ?v_271) x_67) ?v_303)) (and (and (and (and (and (and (and (and (and (= x_78 2) ?v_286) ?v_299) x_49) x_63) ?v_292) ?v_300) x_66) x_67) ?v_301)) (and (and (and (and (and (and (and (and (= x_78 3) ?v_286) x_48) x_49) x_73) ?v_302) ?v_271) ?v_269) ?v_303)) (and (and (and (and (and (and (and (= x_78 4) ?v_293) (or (or ?v_299 x_49) ?v_304)) (or (or ?v_299 ?v_297) ?v_304)) (= x_75 ?v_305)) (= x_73 x_55)) (= x_74 x_56)) ?v_306)) (and (and (and (and (and (and (= x_78 5) ?v_286) ?v_288) x_64) ?v_303) ?v_300) ?v_306))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_79 0) ?v_286) ?v_309) ?v_307) ?v_298) ?v_302) x_68) ?v_279) ?v_310) ?v_308) (and (and (and (and (and (and (and (= x_79 1) ?v_286) x_50) ?v_307) ?v_281) x_69) ?v_308) ?v_311)) (and (and (and (and (and (and (and (and (and (= x_79 2) ?v_286) ?v_309) x_51) x_73) ?v_302) x_68) x_69) ?v_310) ?v_308)) (and (and (and (and (and (and (and (and (= x_79 3) ?v_286) x_50) x_51) (not (< x_47 1))) ?v_281) ?v_279) ?v_308) ?v_311)) (and (and (and (and (and (and (= x_79 4) ?v_293) (or (or ?v_309 x_51) (<= ?v_312 1))) (or (or ?v_309 ?v_307) (<= ?v_312 2))) (= x_65 ?v_312)) ?v_313) ?v_308)) (and (and (and (and (and (and (= x_79 5) ?v_286) ?v_298) x_74) ?v_311) ?v_313) ?v_308))) (= x_58 (ite ?v_321 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_59 0) ?v_314) ?v_317) ?v_315) ?v_316) ?v_320) x_52) ?v_287) (= x_54 0)) (and (and (and (and (and (and (and (and (= x_59 1) ?v_314) x_30) ?v_315) (not (<= x_32 2))) ?v_318) ?v_289) x_53) ?v_319)) (and (and (and (and (and (and (and (= x_59 2) ?v_314) ?v_317) x_31) ?v_318) x_52) x_53) ?v_319)) (and (and (and (and (and (and (and (and (= x_59 3) ?v_314) x_30) x_31) x_45) ?v_320) ?v_289) ?v_287) ?v_319)) (and (and (and (and (and (and (and (and (= x_59 4) ?v_321) (or (or ?v_317 x_31) ?v_322)) (or (or x_30 ?v_315) ?v_322)) (or (or ?v_317 ?v_315) ?v_322)) (= x_54 ?v_323)) (= x_45 x_22)) (= x_46 x_23)) ?v_324)) (and (and (and (and (= x_59 5) ?v_314) ?v_319) ?v_318) ?v_324))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_60 0) ?v_314) ?v_327) ?v_325) ?v_316) ?v_320) ?v_328) x_48) ?v_297) ?v_329) (and (and (and (and (and (and (and (and (and (= x_60 1) ?v_314) x_25) ?v_325) (= x_35 1)) ?v_326) ?v_330) ?v_299) x_49) ?v_331)) (and (and (and (and (and (and (and (and (and (= x_60 2) ?v_314) ?v_327) x_26) x_45) ?v_320) ?v_328) x_48) x_49) ?v_329)) (and (and (and (and (and (and (and (and (= x_60 3) ?v_314) x_25) x_26) x_55) ?v_330) ?v_299) ?v_297) ?v_331)) (and (and (and (and (and (and (and (= x_60 4) ?v_321) (or (or ?v_327 x_26) ?v_332)) (or (or ?v_327 ?v_325) ?v_332)) (= x_57 ?v_333)) (= x_55 x_33)) (= x_56 x_34)) ?v_334)) (and (and (and (and (and (and (= x_60 5) ?v_314) ?v_316) x_46) ?v_331) ?v_328) ?v_334))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_61 0) ?v_314) ?v_337) ?v_335) ?v_326) ?v_330) x_50) ?v_307) ?v_338) ?v_336) (and (and (and (and (and (and (and (= x_61 1) ?v_314) x_28) ?v_335) ?v_309) x_51) ?v_336) ?v_339)) (and (and (and (and (and (and (and (and (and (= x_61 2) ?v_314) ?v_337) x_29) x_55) ?v_330) x_50) x_51) ?v_338) ?v_336)) (and (and (and (and (and (and (and (and (= x_61 3) ?v_314) x_28) x_29) (not (< x_24 1))) ?v_309) ?v_307) ?v_336) ?v_339)) (and (and (and (and (and (and (= x_61 4) ?v_321) (or (or ?v_337 x_29) (<= ?v_340 1))) (or (or ?v_337 ?v_335) (<= ?v_340 2))) (= x_47 ?v_340)) ?v_341) ?v_336)) (and (and (and (and (and (and (= x_61 5) ?v_314) ?v_326) x_56) ?v_339) ?v_341) ?v_336))) (= x_36 (ite x_27 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_37 0) ?v_344) ?v_342) ?v_343) ?v_345) ?v_348) x_30) ?v_315) ?v_346) (and (and (and (and (and (and (and (and (= x_37 1) ?v_344) x_0) ?v_343) (not (<= 0 2))) ?v_347) ?v_317) x_31) ?v_346)) (and (and (and (and (and (and (and (= x_37 2) ?v_344) ?v_342) x_1) ?v_347) x_30) x_31) ?v_346)) (and (and (and (and (and (and (and (and (= x_37 3) ?v_344) x_0) x_1) x_22) ?v_348) ?v_317) ?v_315) ?v_346)) (and (and (and (and (and (and (and (and (= x_37 4) x_27) (or (or ?v_342 x_1) ?v_349)) (or (or x_0 ?v_343) ?v_349)) (or (or ?v_342 ?v_343) ?v_349)) (= x_32 ?v_350)) (= x_22 x_38)) (= x_23 x_39)) ?v_351)) (and (and (and (and (= x_37 5) ?v_344) ?v_346) ?v_347) ?v_351))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_40 0) ?v_344) ?v_352) ?v_353) ?v_345) ?v_348) ?v_356) x_25) ?v_325) ?v_355) (and (and (and (and (and (and (and (and (and (= x_40 1) ?v_344) x_2) ?v_353) (= 0 1)) ?v_354) ?v_357) ?v_327) x_26) ?v_355)) (and (and (and (and (and (and (and (and (and (= x_40 2) ?v_344) ?v_352) x_3) x_22) ?v_348) ?v_356) x_25) x_26) ?v_355)) (and (and (and (and (and (and (and (and (= x_40 3) ?v_344) x_2) x_3) x_33) ?v_357) ?v_327) ?v_325) ?v_355)) (and (and (and (and (and (and (and (= x_40 4) x_27) (or (or ?v_352 x_3) ?v_358)) (or (or ?v_352 ?v_353) ?v_358)) (= x_35 ?v_350)) (= x_33 x_41)) (= x_34 x_42)) ?v_359)) (and (and (and (and (and (and (= x_40 5) ?v_344) ?v_345) x_23) ?v_355) ?v_356) ?v_359))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_43 0) ?v_344) ?v_360) ?v_361) ?v_354) ?v_357) x_28) ?v_335) ?v_363) ?v_362) (and (and (and (and (and (and (and (= x_43 1) ?v_344) x_4) ?v_361) ?v_337) x_29) ?v_362) ?v_363)) (and (and (and (and (and (and (and (and (and (= x_43 2) ?v_344) ?v_360) x_5) x_33) ?v_357) x_28) x_29) ?v_363) ?v_362)) (and (and (and (and (and (and (and (and (= x_43 3) ?v_344) x_4) x_5) (not (< 0 1))) ?v_337) ?v_335) ?v_362) ?v_363)) (and (and (and (and (and (and (= x_43 4) x_27) (or (or ?v_360 x_5) ?v_358)) (or (or ?v_360 ?v_361) (<= ?v_350 2))) (= x_24 ?v_350)) ?v_364) ?v_362)) (and (and (and (and (and (and (= x_43 5) ?v_344) ?v_354) x_34) ?v_363) ?v_364) ?v_362))) (or (or (or (or (or (or (or (or (or (or (or (or (or (and (and ?v_7 x_251) (or x_248 ?v_30)) (and (and ?v_3 x_233) (or x_230 ?v_25))) (and (and ?v_37 x_215) (or x_212 ?v_55))) (and (and ?v_65 x_197) (or x_194 ?v_83))) (and (and ?v_93 x_179) (or x_176 ?v_111))) (and (and ?v_121 x_161) (or x_158 ?v_139))) (and (and ?v_149 x_143) (or x_140 ?v_167))) (and (and ?v_177 x_125) (or x_122 ?v_195))) (and (and ?v_205 x_107) (or x_104 ?v_223))) (and (and ?v_233 x_89) (or x_86 ?v_251))) (and (and ?v_261 x_71) (or x_68 ?v_279))) (and (and ?v_289 x_53) (or x_50 ?v_307))) (and (and ?v_317 x_31) (or x_28 ?v_335))) (and (and ?v_342 x_1) (or x_4 ?v_361)))) (or ?v_348 ?v_345)) (or ?v_357 ?v_354)) (or (not x_39) (not x_38))) (or (not x_42) (not x_41))) (or ?v_320 ?v_316)) (or ?v_330 ?v_326)) (or ?v_292 ?v_288)) (or ?v_302 ?v_298)) (or ?v_264 ?v_260)) (or ?v_274 ?v_270)) (or ?v_236 ?v_232)) (or ?v_246 ?v_242)) (or ?v_208 ?v_204)) (or ?v_218 ?v_214)) (or ?v_180 ?v_176)) (or ?v_190 ?v_186)) (or ?v_152 ?v_148)) (or ?v_162 ?v_158)) (or ?v_124 ?v_120)) (or ?v_134 ?v_130)) (or ?v_96 ?v_92)) (or ?v_106 ?v_102)) (or ?v_68 ?v_64)) (or ?v_78 ?v_74)) (or ?v_40 ?v_36)) (or ?v_50 ?v_46)) (or ?v_6 ?v_2)) (or ?v_18 ?v_14))))))))))))))))))))))))))))))
(check-sat)
(exit)
